$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it as}$,${\it bs}$:($T$ List).
\\[0ex]no\_repeats($T$; ${\it as}$) $\Rightarrow$ no\_repeats($T$; l{-}union(${\it eq}$; ${\it as}$; ${\it bs}$))